M.pre(a,s) == P != (M.2.2.2).1(a)  (P(s)) 

latex

---

clarification:

M.pre(a,s) == fpf-val(IdDeq; ((M.2.2.2).1); a; a,P.((P(s)))) 

latex

Definitions	z != f(x)  P(a;z), IdDeq, t.1, t.2, b, f(a)
FDL editor aliases	ma-pre